Problem:
a__nats() -> a__adx(a__zeros())
a__zeros() -> cons(0(),zeros())
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(adx(X)) -> a__adx(mark(X))
mark(zeros()) -> a__zeros()
mark(incr(X)) -> a__incr(mark(X))
mark(hd(X)) -> a__hd(mark(X))
mark(tl(X)) -> a__tl(mark(X))
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__nats() -> nats()
a__adx(X) -> adx(X)
a__zeros() -> zeros()
a__incr(X) -> incr(X)
a__hd(X) -> hd(X)
a__tl(X) -> tl(X)
Proof:
Complexity Transformation Processor:
strict:
a__nats() -> a__adx(a__zeros())
a__zeros() -> cons(0(),zeros())
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(adx(X)) -> a__adx(mark(X))
mark(zeros()) -> a__zeros()
mark(incr(X)) -> a__incr(mark(X))
mark(hd(X)) -> a__hd(mark(X))
mark(tl(X)) -> a__tl(mark(X))
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__nats() -> nats()
a__adx(X) -> adx(X)
a__zeros() -> zeros()
a__incr(X) -> incr(X)
a__hd(X) -> hd(X)
a__tl(X) -> tl(X)
weak:
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[tl](x0) = x0 + 16,
[hd](x0) = x0 + 11,
[nats] = 12,
[a__tl](x0) = x0 + 17,
[mark](x0) = x0 + 25,
[a__hd](x0) = x0 + 3,
[adx](x0) = x0 + 1,
[incr](x0) = x0 + 12,
[s](x0) = x0 + 4,
[a__incr](x0) = x0 + 2,
[cons](x0, x1) = x0 + x1 + 25,
[zeros] = 0,
[0] = 2,
[a__adx](x0) = x0 + 11,
[a__zeros] = 22,
[a__nats] = 0
orientation:
a__nats() = 0 >= 33 = a__adx(a__zeros())
a__zeros() = 22 >= 27 = cons(0(),zeros())
a__incr(cons(X,Y)) = X + Y + 27 >= X + Y + 41 = cons(s(X),incr(Y))
a__adx(cons(X,Y)) = X + Y + 36 >= X + Y + 28 = a__incr(cons(X,adx(Y)))
a__hd(cons(X,Y)) = X + Y + 28 >= X + 25 = mark(X)
a__tl(cons(X,Y)) = X + Y + 42 >= Y + 25 = mark(Y)
mark(nats()) = 37 >= 0 = a__nats()
mark(adx(X)) = X + 26 >= X + 36 = a__adx(mark(X))
mark(zeros()) = 25 >= 22 = a__zeros()
mark(incr(X)) = X + 37 >= X + 27 = a__incr(mark(X))
mark(hd(X)) = X + 36 >= X + 28 = a__hd(mark(X))
mark(tl(X)) = X + 41 >= X + 42 = a__tl(mark(X))
mark(cons(X1,X2)) = X1 + X2 + 50 >= X1 + X2 + 25 = cons(X1,X2)
mark(0()) = 27 >= 2 = 0()
mark(s(X)) = X + 29 >= X + 4 = s(X)
a__nats() = 0 >= 12 = nats()
a__adx(X) = X + 11 >= X + 1 = adx(X)
a__zeros() = 22 >= 0 = zeros()
a__incr(X) = X + 2 >= X + 12 = incr(X)
a__hd(X) = X + 3 >= X + 11 = hd(X)
a__tl(X) = X + 17 >= X + 16 = tl(X)
problem:
strict:
a__nats() -> a__adx(a__zeros())
a__zeros() -> cons(0(),zeros())
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
mark(adx(X)) -> a__adx(mark(X))
mark(tl(X)) -> a__tl(mark(X))
a__nats() -> nats()
a__incr(X) -> incr(X)
a__hd(X) -> hd(X)
weak:
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(zeros()) -> a__zeros()
mark(incr(X)) -> a__incr(mark(X))
mark(hd(X)) -> a__hd(mark(X))
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__adx(X) -> adx(X)
a__zeros() -> zeros()
a__tl(X) -> tl(X)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[tl](x0) = x0,
[hd](x0) = x0,
[nats] = 15,
[a__tl](x0) = x0,
[mark](x0) = x0,
[a__hd](x0) = x0,
[adx](x0) = x0 + 2,
[incr](x0) = x0,
[s](x0) = x0 + 7,
[a__incr](x0) = x0,
[cons](x0, x1) = x0 + x1,
[zeros] = 0,
[0] = 2,
[a__adx](x0) = x0 + 2,
[a__zeros] = 0,
[a__nats] = 15
orientation:
a__nats() = 15 >= 2 = a__adx(a__zeros())
a__zeros() = 0 >= 2 = cons(0(),zeros())
a__incr(cons(X,Y)) = X + Y >= X + Y + 7 = cons(s(X),incr(Y))
mark(adx(X)) = X + 2 >= X + 2 = a__adx(mark(X))
mark(tl(X)) = X >= X = a__tl(mark(X))
a__nats() = 15 >= 15 = nats()
a__incr(X) = X >= X = incr(X)
a__hd(X) = X >= X = hd(X)
a__adx(cons(X,Y)) = X + Y + 2 >= X + Y + 2 = a__incr(cons(X,adx(Y)))
a__hd(cons(X,Y)) = X + Y >= X = mark(X)
a__tl(cons(X,Y)) = X + Y >= Y = mark(Y)
mark(nats()) = 15 >= 15 = a__nats()
mark(zeros()) = 0 >= 0 = a__zeros()
mark(incr(X)) = X >= X = a__incr(mark(X))
mark(hd(X)) = X >= X = a__hd(mark(X))
mark(cons(X1,X2)) = X1 + X2 >= X1 + X2 = cons(X1,X2)
mark(0()) = 2 >= 2 = 0()
mark(s(X)) = X + 7 >= X + 7 = s(X)
a__adx(X) = X + 2 >= X + 2 = adx(X)
a__zeros() = 0 >= 0 = zeros()
a__tl(X) = X >= X = tl(X)
problem:
strict:
a__zeros() -> cons(0(),zeros())
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
mark(adx(X)) -> a__adx(mark(X))
mark(tl(X)) -> a__tl(mark(X))
a__nats() -> nats()
a__incr(X) -> incr(X)
a__hd(X) -> hd(X)
weak:
a__nats() -> a__adx(a__zeros())
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(zeros()) -> a__zeros()
mark(incr(X)) -> a__incr(mark(X))
mark(hd(X)) -> a__hd(mark(X))
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__adx(X) -> adx(X)
a__zeros() -> zeros()
a__tl(X) -> tl(X)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[tl](x0) = x0,
[hd](x0) = x0 + 12,
[nats] = 13,
[a__tl](x0) = x0 + 6,
[mark](x0) = x0 + 11,
[a__hd](x0) = x0 + 4,
[adx](x0) = x0,
[incr](x0) = x0 + 11,
[s](x0) = x0 + 6,
[a__incr](x0) = x0 + 2,
[cons](x0, x1) = x0 + x1 + 7,
[zeros] = 9,
[0] = 12,
[a__adx](x0) = x0 + 2,
[a__zeros] = 13,
[a__nats] = 15
orientation:
a__zeros() = 13 >= 28 = cons(0(),zeros())
a__incr(cons(X,Y)) = X + Y + 9 >= X + Y + 24 = cons(s(X),incr(Y))
mark(adx(X)) = X + 11 >= X + 13 = a__adx(mark(X))
mark(tl(X)) = X + 11 >= X + 17 = a__tl(mark(X))
a__nats() = 15 >= 13 = nats()
a__incr(X) = X + 2 >= X + 11 = incr(X)
a__hd(X) = X + 4 >= X + 12 = hd(X)
a__nats() = 15 >= 15 = a__adx(a__zeros())
a__adx(cons(X,Y)) = X + Y + 9 >= X + Y + 9 = a__incr(cons(X,adx(Y)))
a__hd(cons(X,Y)) = X + Y + 11 >= X + 11 = mark(X)
a__tl(cons(X,Y)) = X + Y + 13 >= Y + 11 = mark(Y)
mark(nats()) = 24 >= 15 = a__nats()
mark(zeros()) = 20 >= 13 = a__zeros()
mark(incr(X)) = X + 22 >= X + 13 = a__incr(mark(X))
mark(hd(X)) = X + 23 >= X + 15 = a__hd(mark(X))
mark(cons(X1,X2)) = X1 + X2 + 18 >= X1 + X2 + 7 = cons(X1,X2)
mark(0()) = 23 >= 12 = 0()
mark(s(X)) = X + 17 >= X + 6 = s(X)
a__adx(X) = X + 2 >= X = adx(X)
a__zeros() = 13 >= 9 = zeros()
a__tl(X) = X + 6 >= X = tl(X)
problem:
strict:
a__zeros() -> cons(0(),zeros())
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
mark(adx(X)) -> a__adx(mark(X))
mark(tl(X)) -> a__tl(mark(X))
a__incr(X) -> incr(X)
a__hd(X) -> hd(X)
weak:
a__nats() -> nats()
a__nats() -> a__adx(a__zeros())
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(zeros()) -> a__zeros()
mark(incr(X)) -> a__incr(mark(X))
mark(hd(X)) -> a__hd(mark(X))
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__adx(X) -> adx(X)
a__zeros() -> zeros()
a__tl(X) -> tl(X)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[tl](x0) = x0 + 4,
[hd](x0) = x0 + 2,
[nats] = 0,
[a__tl](x0) = x0 + 4,
[mark](x0) = x0 + 1,
[a__hd](x0) = x0 + 2,
[adx](x0) = x0,
[incr](x0) = x0,
[s](x0) = x0 + 1,
[a__incr](x0) = x0,
[cons](x0, x1) = x0 + x1,
[zeros] = 0,
[0] = 0,
[a__adx](x0) = x0,
[a__zeros] = 1,
[a__nats] = 1
orientation:
a__zeros() = 1 >= 0 = cons(0(),zeros())
a__incr(cons(X,Y)) = X + Y >= X + Y + 1 = cons(s(X),incr(Y))
mark(adx(X)) = X + 1 >= X + 1 = a__adx(mark(X))
mark(tl(X)) = X + 5 >= X + 5 = a__tl(mark(X))
a__incr(X) = X >= X = incr(X)
a__hd(X) = X + 2 >= X + 2 = hd(X)
a__nats() = 1 >= 0 = nats()
a__nats() = 1 >= 1 = a__adx(a__zeros())
a__adx(cons(X,Y)) = X + Y >= X + Y = a__incr(cons(X,adx(Y)))
a__hd(cons(X,Y)) = X + Y + 2 >= X + 1 = mark(X)
a__tl(cons(X,Y)) = X + Y + 4 >= Y + 1 = mark(Y)
mark(nats()) = 1 >= 1 = a__nats()
mark(zeros()) = 1 >= 1 = a__zeros()
mark(incr(X)) = X + 1 >= X + 1 = a__incr(mark(X))
mark(hd(X)) = X + 3 >= X + 3 = a__hd(mark(X))
mark(cons(X1,X2)) = X1 + X2 + 1 >= X1 + X2 = cons(X1,X2)
mark(0()) = 1 >= 0 = 0()
mark(s(X)) = X + 2 >= X + 1 = s(X)
a__adx(X) = X >= X = adx(X)
a__zeros() = 1 >= 0 = zeros()
a__tl(X) = X + 4 >= X + 4 = tl(X)
problem:
strict:
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
mark(adx(X)) -> a__adx(mark(X))
mark(tl(X)) -> a__tl(mark(X))
a__incr(X) -> incr(X)
a__hd(X) -> hd(X)
weak:
a__zeros() -> cons(0(),zeros())
a__nats() -> nats()
a__nats() -> a__adx(a__zeros())
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(zeros()) -> a__zeros()
mark(incr(X)) -> a__incr(mark(X))
mark(hd(X)) -> a__hd(mark(X))
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__adx(X) -> adx(X)
a__zeros() -> zeros()
a__tl(X) -> tl(X)
Matrix Interpretation Processor:
dimension: 3
max_matrix:
[1 1 1]
[0 0 0]
[0 0 1]
interpretation:
[1 0 1] [1]
[tl](x0) = [0 0 0]x0 + [0]
[0 0 1] [0],
[1 1 0] [0]
[hd](x0) = [0 0 0]x0 + [0]
[0 0 1] [1],
[1]
[nats] = [0]
[1],
[1 1 1] [1]
[a__tl](x0) = [0 0 0]x0 + [0]
[0 0 1] [0],
[1 0 1]
[mark](x0) = [0 0 0]x0
[0 0 1] ,
[1 1 0] [1]
[a__hd](x0) = [0 0 0]x0 + [0]
[0 0 1] [1],
[1 0 0]
[adx](x0) = [0 0 0]x0
[0 0 1] ,
[1 0 0]
[incr](x0) = [0 0 0]x0
[0 0 1] ,
[1 0 1]
[s](x0) = [0 0 0]x0
[0 0 0] ,
[1 0 0]
[a__incr](x0) = [0 0 0]x0
[0 0 1] ,
[1 0 1] [1 0 0]
[cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1
[0 0 1] [0 0 1] ,
[0]
[zeros] = [0]
[0],
[0]
[0] = [0]
[0],
[1 1 0]
[a__adx](x0) = [0 0 0]x0
[0 0 1] ,
[0]
[a__zeros] = [0]
[0],
[1]
[a__nats] = [0]
[1]
orientation:
[1 0 1] [1 0 0] [1 0 1] [1 0 0]
a__incr(cons(X,Y)) = [0 0 0]X + [0 0 0]Y >= [0 0 0]X + [0 0 0]Y = cons(s(X),incr(Y))
[0 0 1] [0 0 1] [0 0 0] [0 0 1]
[1 0 1] [1 0 1]
mark(adx(X)) = [0 0 0]X >= [0 0 0]X = a__adx(mark(X))
[0 0 1] [0 0 1]
[1 0 2] [1] [1 0 2] [1]
mark(tl(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = a__tl(mark(X))
[0 0 1] [0] [0 0 1] [0]
[1 0 0] [1 0 0]
a__incr(X) = [0 0 0]X >= [0 0 0]X = incr(X)
[0 0 1] [0 0 1]
[1 1 0] [1] [1 1 0] [0]
a__hd(X) = [0 0 0]X + [0] >= [0 0 0]X + [0] = hd(X)
[0 0 1] [1] [0 0 1] [1]
[0] [0]
a__zeros() = [0] >= [0] = cons(0(),zeros())
[0] [0]
[1] [1]
a__nats() = [0] >= [0] = nats()
[1] [1]
[1] [0]
a__nats() = [0] >= [0] = a__adx(a__zeros())
[1] [0]
[1 0 1] [1 0 0] [1 0 1] [1 0 0]
a__adx(cons(X,Y)) = [0 0 0]X + [0 0 0]Y >= [0 0 0]X + [0 0 0]Y = a__incr(cons(X,adx(Y)))
[0 0 1] [0 0 1] [0 0 1] [0 0 1]
[1 0 1] [1 0 0] [1] [1 0 1]
a__hd(cons(X,Y)) = [0 0 0]X + [0 0 0]Y + [0] >= [0 0 0]X = mark(X)
[0 0 1] [0 0 1] [1] [0 0 1]
[1 0 2] [1 0 1] [1] [1 0 1]
a__tl(cons(X,Y)) = [0 0 0]X + [0 0 0]Y + [0] >= [0 0 0]Y = mark(Y)
[0 0 1] [0 0 1] [0] [0 0 1]
[2] [1]
mark(nats()) = [0] >= [0] = a__nats()
[1] [1]
[0] [0]
mark(zeros()) = [0] >= [0] = a__zeros()
[0] [0]
[1 0 1] [1 0 1]
mark(incr(X)) = [0 0 0]X >= [0 0 0]X = a__incr(mark(X))
[0 0 1] [0 0 1]
[1 1 1] [1] [1 0 1] [1]
mark(hd(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = a__hd(mark(X))
[0 0 1] [1] [0 0 1] [1]
[1 0 2] [1 0 1] [1 0 1] [1 0 0]
mark(cons(X1,X2)) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = cons(X1,X2)
[0 0 1] [0 0 1] [0 0 1] [0 0 1]
[0] [0]
mark(0()) = [0] >= [0] = 0()
[0] [0]
[1 0 1] [1 0 1]
mark(s(X)) = [0 0 0]X >= [0 0 0]X = s(X)
[0 0 0] [0 0 0]
[1 1 0] [1 0 0]
a__adx(X) = [0 0 0]X >= [0 0 0]X = adx(X)
[0 0 1] [0 0 1]
[0] [0]
a__zeros() = [0] >= [0] = zeros()
[0] [0]
[1 1 1] [1] [1 0 1] [1]
a__tl(X) = [0 0 0]X + [0] >= [0 0 0]X + [0] = tl(X)
[0 0 1] [0] [0 0 1] [0]
problem:
strict:
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
mark(adx(X)) -> a__adx(mark(X))
mark(tl(X)) -> a__tl(mark(X))
a__incr(X) -> incr(X)
weak:
a__hd(X) -> hd(X)
a__zeros() -> cons(0(),zeros())
a__nats() -> nats()
a__nats() -> a__adx(a__zeros())
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(zeros()) -> a__zeros()
mark(incr(X)) -> a__incr(mark(X))
mark(hd(X)) -> a__hd(mark(X))
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__adx(X) -> adx(X)
a__zeros() -> zeros()
a__tl(X) -> tl(X)
Matrix Interpretation Processor:
dimension: 3
max_matrix:
[1 1 1]
[0 0 1]
[0 0 1]
interpretation:
[1 0 0] [0]
[tl](x0) = [0 0 1]x0 + [0]
[0 0 1] [1],
[1 0 0]
[hd](x0) = [0 0 0]x0
[0 0 1] ,
[0]
[nats] = [0]
[1],
[1 0 0] [0]
[a__tl](x0) = [0 0 1]x0 + [1]
[0 0 1] [1],
[1 0 1]
[mark](x0) = [0 0 1]x0
[0 0 1] ,
[1 0 0]
[a__hd](x0) = [0 0 1]x0
[0 0 1] ,
[1 0 0]
[adx](x0) = [0 0 0]x0
[0 0 1] ,
[1 0 0]
[incr](x0) = [0 0 0]x0
[0 0 1] ,
[1 0 0]
[s](x0) = [0 0 0]x0
[0 0 0] ,
[1 0 0]
[a__incr](x0) = [0 0 0]x0
[0 0 1] ,
[1 1 1] [1 0 1]
[cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1
[0 0 1] [0 0 1] ,
[0]
[zeros] = [0]
[1],
[0]
[0] = [0]
[0],
[1 0 0]
[a__adx](x0) = [0 0 0]x0
[0 0 1] ,
[1]
[a__zeros] = [0]
[1],
[1]
[a__nats] = [0]
[1]
orientation:
[1 1 1] [1 0 1] [1 0 0] [1 0 1]
a__incr(cons(X,Y)) = [0 0 0]X + [0 0 0]Y >= [0 0 0]X + [0 0 0]Y = cons(s(X),incr(Y))
[0 0 1] [0 0 1] [0 0 0] [0 0 1]
[1 0 1] [1 0 1]
mark(adx(X)) = [0 0 1]X >= [0 0 0]X = a__adx(mark(X))
[0 0 1] [0 0 1]
[1 0 1] [1] [1 0 1] [0]
mark(tl(X)) = [0 0 1]X + [1] >= [0 0 1]X + [1] = a__tl(mark(X))
[0 0 1] [1] [0 0 1] [1]
[1 0 0] [1 0 0]
a__incr(X) = [0 0 0]X >= [0 0 0]X = incr(X)
[0 0 1] [0 0 1]
[1 0 0] [1 0 0]
a__hd(X) = [0 0 1]X >= [0 0 0]X = hd(X)
[0 0 1] [0 0 1]
[1] [1]
a__zeros() = [0] >= [0] = cons(0(),zeros())
[1] [1]
[1] [0]
a__nats() = [0] >= [0] = nats()
[1] [1]
[1] [1]
a__nats() = [0] >= [0] = a__adx(a__zeros())
[1] [1]
[1 1 1] [1 0 1] [1 1 1] [1 0 1]
a__adx(cons(X,Y)) = [0 0 0]X + [0 0 0]Y >= [0 0 0]X + [0 0 0]Y = a__incr(cons(X,adx(Y)))
[0 0 1] [0 0 1] [0 0 1] [0 0 1]
[1 1 1] [1 0 1] [1 0 1]
a__hd(cons(X,Y)) = [0 0 1]X + [0 0 1]Y >= [0 0 1]X = mark(X)
[0 0 1] [0 0 1] [0 0 1]
[1 1 1] [1 0 1] [0] [1 0 1]
a__tl(cons(X,Y)) = [0 0 1]X + [0 0 1]Y + [1] >= [0 0 1]Y = mark(Y)
[0 0 1] [0 0 1] [1] [0 0 1]
[1] [1]
mark(nats()) = [1] >= [0] = a__nats()
[1] [1]
[1] [1]
mark(zeros()) = [1] >= [0] = a__zeros()
[1] [1]
[1 0 1] [1 0 1]
mark(incr(X)) = [0 0 1]X >= [0 0 0]X = a__incr(mark(X))
[0 0 1] [0 0 1]
[1 0 1] [1 0 1]
mark(hd(X)) = [0 0 1]X >= [0 0 1]X = a__hd(mark(X))
[0 0 1] [0 0 1]
[1 1 2] [1 0 2] [1 1 1] [1 0 1]
mark(cons(X1,X2)) = [0 0 1]X1 + [0 0 1]X2 >= [0 0 0]X1 + [0 0 0]X2 = cons(X1,X2)
[0 0 1] [0 0 1] [0 0 1] [0 0 1]
[0] [0]
mark(0()) = [0] >= [0] = 0()
[0] [0]
[1 0 0] [1 0 0]
mark(s(X)) = [0 0 0]X >= [0 0 0]X = s(X)
[0 0 0] [0 0 0]
[1 0 0] [1 0 0]
a__adx(X) = [0 0 0]X >= [0 0 0]X = adx(X)
[0 0 1] [0 0 1]
[1] [0]
a__zeros() = [0] >= [0] = zeros()
[1] [1]
[1 0 0] [0] [1 0 0] [0]
a__tl(X) = [0 0 1]X + [1] >= [0 0 1]X + [0] = tl(X)
[0 0 1] [1] [0 0 1] [1]
problem:
strict:
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
mark(adx(X)) -> a__adx(mark(X))
a__incr(X) -> incr(X)
weak:
mark(tl(X)) -> a__tl(mark(X))
a__hd(X) -> hd(X)
a__zeros() -> cons(0(),zeros())
a__nats() -> nats()
a__nats() -> a__adx(a__zeros())
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(zeros()) -> a__zeros()
mark(incr(X)) -> a__incr(mark(X))
mark(hd(X)) -> a__hd(mark(X))
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__adx(X) -> adx(X)
a__zeros() -> zeros()
a__tl(X) -> tl(X)
Matrix Interpretation Processor:
dimension: 3
max_matrix:
[1 1 1]
[0 0 0]
[0 0 1]
interpretation:
[1 0 1]
[tl](x0) = [0 0 0]x0
[0 0 1] ,
[1 0 0]
[hd](x0) = [0 0 0]x0
[0 0 1] ,
[0]
[nats] = [0]
[1],
[1 0 1]
[a__tl](x0) = [0 0 0]x0
[0 0 1] ,
[1 0 1]
[mark](x0) = [0 0 0]x0
[0 0 1] ,
[1 1 0]
[a__hd](x0) = [0 0 0]x0
[0 0 1] ,
[1 0 1] [0]
[adx](x0) = [0 0 0]x0 + [0]
[0 0 1] [1],
[1 0 0]
[incr](x0) = [0 0 0]x0
[0 0 1] ,
[1 1 0]
[s](x0) = [0 0 0]x0
[0 0 0] ,
[1 0 0]
[a__incr](x0) = [0 0 0]x0
[0 0 1] ,
[1 1 1] [1 0 0]
[cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1
[0 0 1] [0 0 1] ,
[1]
[zeros] = [0]
[0],
[0]
[0] = [0]
[0],
[1 0 1] [0]
[a__adx](x0) = [0 0 0]x0 + [0]
[0 0 1] [1],
[1]
[a__zeros] = [0]
[0],
[1]
[a__nats] = [0]
[1]
orientation:
[1 1 1] [1 0 0] [1 1 0] [1 0 0]
a__incr(cons(X,Y)) = [0 0 0]X + [0 0 0]Y >= [0 0 0]X + [0 0 0]Y = cons(s(X),incr(Y))
[0 0 1] [0 0 1] [0 0 0] [0 0 1]
[1 0 2] [1] [1 0 2] [0]
mark(adx(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = a__adx(mark(X))
[0 0 1] [1] [0 0 1] [1]
[1 0 0] [1 0 0]
a__incr(X) = [0 0 0]X >= [0 0 0]X = incr(X)
[0 0 1] [0 0 1]
[1 0 2] [1 0 2]
mark(tl(X)) = [0 0 0]X >= [0 0 0]X = a__tl(mark(X))
[0 0 1] [0 0 1]
[1 1 0] [1 0 0]
a__hd(X) = [0 0 0]X >= [0 0 0]X = hd(X)
[0 0 1] [0 0 1]
[1] [1]
a__zeros() = [0] >= [0] = cons(0(),zeros())
[0] [0]
[1] [0]
a__nats() = [0] >= [0] = nats()
[1] [1]
[1] [1]
a__nats() = [0] >= [0] = a__adx(a__zeros())
[1] [1]
[1 1 2] [1 0 1] [0] [1 1 1] [1 0 1] [0]
a__adx(cons(X,Y)) = [0 0 0]X + [0 0 0]Y + [0] >= [0 0 0]X + [0 0 0]Y + [0] = a__incr(cons(X,adx(Y)))
[0 0 1] [0 0 1] [1] [0 0 1] [0 0 1] [1]
[1 1 1] [1 0 0] [1 0 1]
a__hd(cons(X,Y)) = [0 0 0]X + [0 0 0]Y >= [0 0 0]X = mark(X)
[0 0 1] [0 0 1] [0 0 1]
[1 1 2] [1 0 1] [1 0 1]
a__tl(cons(X,Y)) = [0 0 0]X + [0 0 0]Y >= [0 0 0]Y = mark(Y)
[0 0 1] [0 0 1] [0 0 1]
[1] [1]
mark(nats()) = [0] >= [0] = a__nats()
[1] [1]
[1] [1]
mark(zeros()) = [0] >= [0] = a__zeros()
[0] [0]
[1 0 1] [1 0 1]
mark(incr(X)) = [0 0 0]X >= [0 0 0]X = a__incr(mark(X))
[0 0 1] [0 0 1]
[1 0 1] [1 0 1]
mark(hd(X)) = [0 0 0]X >= [0 0 0]X = a__hd(mark(X))
[0 0 1] [0 0 1]
[1 1 2] [1 0 1] [1 1 1] [1 0 0]
mark(cons(X1,X2)) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = cons(X1,X2)
[0 0 1] [0 0 1] [0 0 1] [0 0 1]
[0] [0]
mark(0()) = [0] >= [0] = 0()
[0] [0]
[1 1 0] [1 1 0]
mark(s(X)) = [0 0 0]X >= [0 0 0]X = s(X)
[0 0 0] [0 0 0]
[1 0 1] [0] [1 0 1] [0]
a__adx(X) = [0 0 0]X + [0] >= [0 0 0]X + [0] = adx(X)
[0 0 1] [1] [0 0 1] [1]
[1] [1]
a__zeros() = [0] >= [0] = zeros()
[0] [0]
[1 0 1] [1 0 1]
a__tl(X) = [0 0 0]X >= [0 0 0]X = tl(X)
[0 0 1] [0 0 1]
problem:
strict:
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
a__incr(X) -> incr(X)
weak:
mark(adx(X)) -> a__adx(mark(X))
mark(tl(X)) -> a__tl(mark(X))
a__hd(X) -> hd(X)
a__zeros() -> cons(0(),zeros())
a__nats() -> nats()
a__nats() -> a__adx(a__zeros())
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(zeros()) -> a__zeros()
mark(incr(X)) -> a__incr(mark(X))
mark(hd(X)) -> a__hd(mark(X))
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__adx(X) -> adx(X)
a__zeros() -> zeros()
a__tl(X) -> tl(X)
Matrix Interpretation Processor:
dimension: 4
max_matrix:
[1 1 1 1]
[0 1 1 1]
[0 0 0 0]
[0 0 0 1]
interpretation:
[1 1 1 1] [1]
[0 1 1 1] [1]
[tl](x0) = [0 0 0 0]x0 + [0]
[0 0 0 1] [1],
[1 0 1 0] [1]
[0 1 1 1] [0]
[hd](x0) = [0 0 0 0]x0 + [0]
[0 0 0 1] [1],
[0]
[1]
[nats] = [0]
[1],
[1 1 1 1] [1]
[0 1 1 1] [1]
[a__tl](x0) = [0 0 0 0]x0 + [0]
[0 0 0 1] [1],
[1 1 0 1]
[0 1 0 1]
[mark](x0) = [0 0 0 0]x0
[0 0 0 1] ,
[1 0 1 0] [1]
[0 1 1 1] [0]
[a__hd](x0) = [0 0 0 0]x0 + [0]
[0 0 0 1] [1],
[1 0 0 0] [0]
[0 1 0 0] [0]
[adx](x0) = [0 0 0 0]x0 + [0]
[0 0 0 1] [1],
[1 0 0 0] [0]
[0 1 0 0] [1]
[incr](x0) = [0 0 0 0]x0 + [0]
[0 0 0 1] [0],
[1 0 0 1] [1]
[0 0 0 0] [0]
[s](x0) = [0 0 0 0]x0 + [0]
[0 0 0 0] [0],
[1 0 0 0] [1]
[0 1 0 0] [1]
[a__incr](x0) = [0 0 0 0]x0 + [0]
[0 0 0 1] [0],
[1 1 0 1] [1 0 0 0]
[0 1 1 0] [0 1 0 0]
[cons](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1
[0 0 0 1] [0 0 0 1] ,
[0]
[0]
[zeros] = [0]
[0],
[0]
[0]
[0] = [0]
[0],
[1 0 1 0] [1]
[0 1 0 0] [1]
[a__adx](x0) = [0 0 0 0]x0 + [0]
[0 0 0 1] [1],
[0]
[0]
[a__zeros] = [0]
[0],
[1]
[1]
[a__nats] = [0]
[1]
orientation:
[1 1 0 1] [1 0 0 0] [1] [1 0 0 1] [1 0 0 0] [1]
[0 1 1 0] [0 1 0 0] [1] [0 0 0 0] [0 1 0 0] [1]
a__incr(cons(X,Y)) = [0 0 0 0]X + [0 0 0 0]Y + [0] >= [0 0 0 0]X + [0 0 0 0]Y + [0] = cons(s(X),incr(Y))
[0 0 0 1] [0 0 0 1] [0] [0 0 0 0] [0 0 0 1] [0]
[1 0 0 0] [1] [1 0 0 0] [0]
[0 1 0 0] [1] [0 1 0 0] [1]
a__incr(X) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = incr(X)
[0 0 0 1] [0] [0 0 0 1] [0]
[1 1 0 1] [1] [1 1 0 1] [1]
[0 1 0 1] [1] [0 1 0 1] [1]
mark(adx(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = a__adx(mark(X))
[0 0 0 1] [1] [0 0 0 1] [1]
[1 2 2 3] [3] [1 2 0 3] [1]
[0 1 1 2] [2] [0 1 0 2] [1]
mark(tl(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = a__tl(mark(X))
[0 0 0 1] [1] [0 0 0 1] [1]
[1 0 1 0] [1] [1 0 1 0] [1]
[0 1 1 1] [0] [0 1 1 1] [0]
a__hd(X) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = hd(X)
[0 0 0 1] [1] [0 0 0 1] [1]
[0] [0]
[0] [0]
a__zeros() = [0] >= [0] = cons(0(),zeros())
[0] [0]
[1] [0]
[1] [1]
a__nats() = [0] >= [0] = nats()
[1] [1]
[1] [1]
[1] [1]
a__nats() = [0] >= [0] = a__adx(a__zeros())
[1] [1]
[1 1 0 1] [1 0 0 0] [1] [1 1 0 1] [1 0 0 0] [1]
[0 1 1 0] [0 1 0 0] [1] [0 1 1 0] [0 1 0 0] [1]
a__adx(cons(X,Y)) = [0 0 0 0]X + [0 0 0 0]Y + [0] >= [0 0 0 0]X + [0 0 0 0]Y + [0] = a__incr(cons(X,adx(Y)))
[0 0 0 1] [0 0 0 1] [1] [0 0 0 1] [0 0 0 1] [1]
[1 1 0 1] [1 0 0 0] [1] [1 1 0 1]
[0 1 1 1] [0 1 0 1] [0] [0 1 0 1]
a__hd(cons(X,Y)) = [0 0 0 0]X + [0 0 0 0]Y + [0] >= [0 0 0 0]X = mark(X)
[0 0 0 1] [0 0 0 1] [1] [0 0 0 1]
[1 2 1 2] [1 1 0 1] [1] [1 1 0 1]
[0 1 1 1] [0 1 0 1] [1] [0 1 0 1]
a__tl(cons(X,Y)) = [0 0 0 0]X + [0 0 0 0]Y + [0] >= [0 0 0 0]Y = mark(Y)
[0 0 0 1] [0 0 0 1] [1] [0 0 0 1]
[2] [1]
[2] [1]
mark(nats()) = [0] >= [0] = a__nats()
[1] [1]
[0] [0]
[0] [0]
mark(zeros()) = [0] >= [0] = a__zeros()
[0] [0]
[1 1 0 1] [1] [1 1 0 1] [1]
[0 1 0 1] [1] [0 1 0 1] [1]
mark(incr(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = a__incr(mark(X))
[0 0 0 1] [0] [0 0 0 1] [0]
[1 1 2 2] [2] [1 1 0 1] [1]
[0 1 1 2] [1] [0 1 0 2] [0]
mark(hd(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = a__hd(mark(X))
[0 0 0 1] [1] [0 0 0 1] [1]
[1 2 1 2] [1 1 0 1] [1 1 0 1] [1 0 0 0]
[0 1 1 1] [0 1 0 1] [0 1 1 0] [0 1 0 0]
mark(cons(X1,X2)) = [0 0 0 0]X1 + [0 0 0 0]X2 >= [0 0 0 0]X1 + [0 0 0 0]X2 = cons(X1,X2)
[0 0 0 1] [0 0 0 1] [0 0 0 1] [0 0 0 1]
[0] [0]
[0] [0]
mark(0()) = [0] >= [0] = 0()
[0] [0]
[1 0 0 1] [1] [1 0 0 1] [1]
[0 0 0 0] [0] [0 0 0 0] [0]
mark(s(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = s(X)
[0 0 0 0] [0] [0 0 0 0] [0]
[1 0 1 0] [1] [1 0 0 0] [0]
[0 1 0 0] [1] [0 1 0 0] [0]
a__adx(X) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = adx(X)
[0 0 0 1] [1] [0 0 0 1] [1]
[0] [0]
[0] [0]
a__zeros() = [0] >= [0] = zeros()
[0] [0]
[1 1 1 1] [1] [1 1 1 1] [1]
[0 1 1 1] [1] [0 1 1 1] [1]
a__tl(X) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = tl(X)
[0 0 0 1] [1] [0 0 0 1] [1]
problem:
strict:
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
weak:
a__incr(X) -> incr(X)
mark(adx(X)) -> a__adx(mark(X))
mark(tl(X)) -> a__tl(mark(X))
a__hd(X) -> hd(X)
a__zeros() -> cons(0(),zeros())
a__nats() -> nats()
a__nats() -> a__adx(a__zeros())
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(zeros()) -> a__zeros()
mark(incr(X)) -> a__incr(mark(X))
mark(hd(X)) -> a__hd(mark(X))
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__adx(X) -> adx(X)
a__zeros() -> zeros()
a__tl(X) -> tl(X)
Matrix Interpretation Processor:
dimension: 4
max_matrix:
[1 1 1 1]
[0 0 0 0]
[0 0 1 1]
[0 0 0 1]
interpretation:
[1 0 1 1] [0]
[0 0 0 0] [1]
[tl](x0) = [0 0 1 1]x0 + [1]
[0 0 0 1] [0],
[1 0 0 1]
[0 0 0 0]
[hd](x0) = [0 0 1 1]x0
[0 0 0 1] ,
[1]
[1]
[nats] = [1]
[1],
[1 0 1 1] [1]
[0 0 0 0] [1]
[a__tl](x0) = [0 0 1 1]x0 + [1]
[0 0 0 1] [0],
[1 0 1 1] [0]
[0 0 0 0] [1]
[mark](x0) = [0 0 1 1]x0 + [0]
[0 0 0 1] [0],
[1 0 0 1] [0]
[0 0 0 0] [1]
[a__hd](x0) = [0 0 1 1]x0 + [0]
[0 0 0 1] [0],
[1 0 0 0] [0]
[0 0 0 0] [0]
[adx](x0) = [0 0 1 0]x0 + [0]
[0 0 0 1] [1],
[1 0 0 0] [0]
[0 0 0 0] [0]
[incr](x0) = [0 0 1 0]x0 + [1]
[0 0 0 1] [0],
[1 0 0 0]
[0 0 0 0]
[s](x0) = [0 0 0 0]x0
[0 0 0 0] ,
[1 1 0 0] [0]
[0 0 0 0] [1]
[a__incr](x0) = [0 0 1 0]x0 + [1]
[0 0 0 1] [0],
[1 0 1 0] [1 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [1]
[cons](x0, x1) = [0 0 1 0]x0 + [0 0 1 0]x1 + [0]
[0 0 0 1] [0 0 0 1] [0],
[0]
[0]
[zeros] = [0]
[0],
[0]
[0]
[0] = [0]
[0],
[1 0 0 0] [1]
[0 0 0 0] [1]
[a__adx](x0) = [0 0 1 0]x0 + [1]
[0 0 0 1] [1],
[0]
[1]
[a__zeros] = [0]
[0],
[1]
[1]
[a__nats] = [1]
[1]
orientation:
[1 0 1 0] [1 0 0 0] [1] [1 0 0 0] [1 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [1] [0 0 0 0] [0 0 0 0] [1]
a__incr(cons(X,Y)) = [0 0 1 0]X + [0 0 1 0]Y + [1] >= [0 0 0 0]X + [0 0 1 0]Y + [1] = cons(s(X),incr(Y))
[0 0 0 1] [0 0 0 1] [0] [0 0 0 0] [0 0 0 1] [0]
[1 1 0 0] [0] [1 0 0 0] [0]
[0 0 0 0] [1] [0 0 0 0] [0]
a__incr(X) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [1] = incr(X)
[0 0 0 1] [0] [0 0 0 1] [0]
[1 0 1 1] [1] [1 0 1 1] [1]
[0 0 0 0] [1] [0 0 0 0] [1]
mark(adx(X)) = [0 0 1 1]X + [1] >= [0 0 1 1]X + [1] = a__adx(mark(X))
[0 0 0 1] [1] [0 0 0 1] [1]
[1 0 2 3] [1] [1 0 2 3] [1]
[0 0 0 0] [1] [0 0 0 0] [1]
mark(tl(X)) = [0 0 1 2]X + [1] >= [0 0 1 2]X + [1] = a__tl(mark(X))
[0 0 0 1] [0] [0 0 0 1] [0]
[1 0 0 1] [0] [1 0 0 1]
[0 0 0 0] [1] [0 0 0 0]
a__hd(X) = [0 0 1 1]X + [0] >= [0 0 1 1]X = hd(X)
[0 0 0 1] [0] [0 0 0 1]
[0] [0]
[1] [1]
a__zeros() = [0] >= [0] = cons(0(),zeros())
[0] [0]
[1] [1]
[1] [1]
a__nats() = [1] >= [1] = nats()
[1] [1]
[1] [1]
[1] [1]
a__nats() = [1] >= [1] = a__adx(a__zeros())
[1] [1]
[1 0 1 0] [1 0 0 0] [1] [1 0 1 0] [1 0 0 0] [1]
[0 0 0 0] [0 0 0 0] [1] [0 0 0 0] [0 0 0 0] [1]
a__adx(cons(X,Y)) = [0 0 1 0]X + [0 0 1 0]Y + [1] >= [0 0 1 0]X + [0 0 1 0]Y + [1] = a__incr(cons(X,adx(Y)))
[0 0 0 1] [0 0 0 1] [1] [0 0 0 1] [0 0 0 1] [1]
[1 0 1 1] [1 0 0 1] [0] [1 0 1 1] [0]
[0 0 0 0] [0 0 0 0] [1] [0 0 0 0] [1]
a__hd(cons(X,Y)) = [0 0 1 1]X + [0 0 1 1]Y + [0] >= [0 0 1 1]X + [0] = mark(X)
[0 0 0 1] [0 0 0 1] [0] [0 0 0 1] [0]
[1 0 2 1] [1 0 1 1] [1] [1 0 1 1] [0]
[0 0 0 0] [0 0 0 0] [1] [0 0 0 0] [1]
a__tl(cons(X,Y)) = [0 0 1 1]X + [0 0 1 1]Y + [1] >= [0 0 1 1]Y + [0] = mark(Y)
[0 0 0 1] [0 0 0 1] [0] [0 0 0 1] [0]
[3] [1]
[1] [1]
mark(nats()) = [2] >= [1] = a__nats()
[1] [1]
[0] [0]
[1] [1]
mark(zeros()) = [0] >= [0] = a__zeros()
[0] [0]
[1 0 1 1] [1] [1 0 1 1] [1]
[0 0 0 0] [1] [0 0 0 0] [1]
mark(incr(X)) = [0 0 1 1]X + [1] >= [0 0 1 1]X + [1] = a__incr(mark(X))
[0 0 0 1] [0] [0 0 0 1] [0]
[1 0 1 3] [0] [1 0 1 2] [0]
[0 0 0 0] [1] [0 0 0 0] [1]
mark(hd(X)) = [0 0 1 2]X + [0] >= [0 0 1 2]X + [0] = a__hd(mark(X))
[0 0 0 1] [0] [0 0 0 1] [0]
[1 0 2 1] [1 0 1 1] [0] [1 0 1 0] [1 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [1] [0 0 0 0] [0 0 0 0] [1]
mark(cons(X1,X2)) = [0 0 1 1]X1 + [0 0 1 1]X2 + [0] >= [0 0 1 0]X1 + [0 0 1 0]X2 + [0] = cons(X1,X2)
[0 0 0 1] [0 0 0 1] [0] [0 0 0 1] [0 0 0 1] [0]
[0] [0]
[1] [0]
mark(0()) = [0] >= [0] = 0()
[0] [0]
[1 0 0 0] [0] [1 0 0 0]
[0 0 0 0] [1] [0 0 0 0]
mark(s(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X = s(X)
[0 0 0 0] [0] [0 0 0 0]
[1 0 0 0] [1] [1 0 0 0] [0]
[0 0 0 0] [1] [0 0 0 0] [0]
a__adx(X) = [0 0 1 0]X + [1] >= [0 0 1 0]X + [0] = adx(X)
[0 0 0 1] [1] [0 0 0 1] [1]
[0] [0]
[1] [0]
a__zeros() = [0] >= [0] = zeros()
[0] [0]
[1 0 1 1] [1] [1 0 1 1] [0]
[0 0 0 0] [1] [0 0 0 0] [1]
a__tl(X) = [0 0 1 1]X + [1] >= [0 0 1 1]X + [1] = tl(X)
[0 0 0 1] [0] [0 0 0 1] [0]
problem:
strict:
weak:
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
a__incr(X) -> incr(X)
mark(adx(X)) -> a__adx(mark(X))
mark(tl(X)) -> a__tl(mark(X))
a__hd(X) -> hd(X)
a__zeros() -> cons(0(),zeros())
a__nats() -> nats()
a__nats() -> a__adx(a__zeros())
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(zeros()) -> a__zeros()
mark(incr(X)) -> a__incr(mark(X))
mark(hd(X)) -> a__hd(mark(X))
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__adx(X) -> adx(X)
a__zeros() -> zeros()
a__tl(X) -> tl(X)
Qed